\begin{tabbing}
$\forall$$w$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ (\=$\forall$$e$:E.\+
\\[0ex]when{-}after($e$;$\lambda$$e$.w{-}info($w$;$e$);$\lambda$$e$.w{-}pred($w$;$e$);$\lambda$$i$,$x$. s($i$;0).$x$;$\lambda$$i$.
\\[0ex]1of(2of(w{-}machine($w$;$i$)));$\lambda$$e$.val($e$))
\\[0ex]$=$
\\[0ex]$\langle$$\lambda$$x$.s(loc($e$);time($e$)).$x$$,\,$$\lambda$$x$.s(loc($e$);time($e$)+1).$x$$\rangle$
\\[0ex]$\in$ ($x$:Id$\rightarrow$$w$.T(loc($e$),$x$))$\times$($x$:Id$\rightarrow$$w$.T(loc($e$),$x$)))
\-
\end{tabbing}